A:Type, f:(A(A + Top)).
SWellFounded(p-graph(A;f)(y,x))
 (x:A.
 n:
 ((can-apply(f^n;x))
 c (final-iterate(f;x) = do-apply(f^n;x)  A & ((can-apply(f;final-iterate(f;x))))))) 

latex

Definitions

Void, t  T, x:A.B(x), Top, Type, x:AB(x), x:A. B(x), , A  B, A, , s = t, S  T, b, can-apply(f;x), , f^n, P  Q, x:A  B(x), P & Q, left + right, suptype(S; T), A c B, final-iterate(f;x), x:A. B(x), n - m, p-id(), True, False, {x:A| B(x)} , s ~ t, {T}, SQType(T), |g|, -n, SWellFounded(R(x;y)), p-graph(A;f), x,y. t(x;y), ff, , b, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], p  q, p  q, p q, tt, Unit, x.A(x), i  j , , #$n, n+m, do-apply(f;x), f(a), a < b

Lemmas

ge wf, nat properties, nat ind tp, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, p-graph wf, strongwellfounded wf, p-fun-exp-add1-sq, final-iterate wf, nat wf, le wf, can-apply wf, do-apply wf, p-fun-exp wf, not wf, assert wf, top wf, member wf